\section{Background}
\label{section:background}


%\subsection{Model Transformations}
\subsection{Transforming Models With Graph Rewriting}
\label{subsec:model_transformations}

\mf{ {\bf Michalis and Levi do} Description of what it means to do model
transformation (very high level)}

\mf{TODO: the following need to be reworded to avoid text replication with
ICSE14}

In this paper we consider models to be attributed, typed graphs.  A {\em
transformation} is a program that takes one model as an input and produces
another model as its output. There are many kinds of model
transformations~\cite{czarnecki03} but in this paper we focus on
transformations based on graph rewriting~\cite{ehrig06}.
The basic building block of such transformations is the {\em transformation
rule}, defined as follows:

\BD[Transformation rule]
A {\em transformation rule} $R$ is a tuple $R=\tuple{\set{$\rp{NAC}$}$,\rp{LHS},\rp{RHS}$}$,
where  \rp{LHS} and \rp{RHS} are the typed graphs called
 the {\em left-hand} and
the {\em right-hand} sides of the rule, respectively, and $\set{\rp{NAC}}$ represents a (potentially
empty) set of typed graphs called the {\em negative application conditions}.
\ED

\mf{TODO: we need an example rule, preferrably from the VCS2Autosar example.}
Fig.~\ref{?} depicts the \rp{NAC}s, \rp{LHS} and \rp{RHS}
of the rule $R_{F}$ from Fig.~\ref{?}
as typed graphs using types from the UML metamodel~\cite{UML10}.
\mf{TODO: update}
For example, \rp{NAC}1 consists of a state \name{x} with an entry action
\name{a1} that is a UML \name{behaviour} (e.g., a class operation).

The \rp{NAC}s, \rp{LHS}, and \rp{RHS} of a rule consist of different {\em parts}, i.e., sets of
model elements which do not necessarily form proper graphs.  These parts play different
roles during the rule application:
\begin{description}
\item [\rC:] The set of model elements that are present both in the \rp{LHS} and the
\rp{RHS}, i.e.,
remain unaffected by the rule.
\item [\rD:] The set of elements in the \rp{LHS} that are absent in the \rp{RHS}, i.e.,
deleted by the rule.
\item [\rA:] The set of elements present in the \rp{RHS} but absent in the \rp{LHS}, i.e.,
added by the rule.
\item [\rN:] The set of elements present in any \rp{NAC},  but not those
present in \rC.
\end{description}


In our example, the parts are as follows: ... 
\mf{TODO, when we agree on example rule}.
% For the example rule $R_{F}$ from Fig.~\ref{fig:foldentry}, these parts are as follows: \rC~is
% $\set{$\name{x},\name{x1},\name{x2},\name{a},\name{t1},\name{t1\_x1},\name{t1\_x},
% \name{t2},\name{t2\_x2},\name{t2\_x}$}$,\\ \rD~is the set
% $\set{$\name{t1\_a},\name{t2\_a}$}$, \rA~is the set $\set{$\name{x\_a}$}$,
% \rN~is set
% $\set{$\name{a1},\name{x\_a1},\name{x3},\name{t3},\name{t3\_x3},\name{t3\_x}$}$.
% To reduce clutter, only \rD and \rA are explicitly indicated in the figure.

A rule $R$ is {\em applied} to a model $M$ by finding a {\em matching site}
of its \rp{LHS} in $M$:
 
\BD[Matching site] \label{def:matchsite}
A \emph{matching site} of a transformation rule $R$ in a model $M$ is a tuple
$K=\tuple{$\mN,\mC,\mD$}$, where \mC~and \mD~are matches of the parts \rC~and
\rD~of the \rp{LHS} of $R$ in $M$, and \mN~is the set of all matches of
\rp{NAC}s in $M$ relative to \mC~and \mD .
\ED

\mf{TODO: once we settle on example, we should illustrate this on the example.
Can reuse commented out latex code.}

% \begin{table}[t!]
% \caption{Matching sites of rule $R_F$ in Fig.~\ref{fig:foldentry} for the domain model in Fig.~\ref{fig:wash}.}
% \label{fig:msites}
% {\small 
% \begin{center}
% \begin{tabular}{|p{0.5cm}|p{1.2cm}|p{3.1cm}|p{2.0cm}|}
% \hline {\bf Site} & {\bf \mN} & {\bf \mC} & {\bf \mD}  \\
% \hline 
% $K_1$ & \name{Washing}, \name{TempCheck}
% & \parbox{3.1cm}{
% \begin{flushleft}
% \vspace{-0cm}
% \name{Washing}, \name{Locking}, \name{Waiting},
% \name{wash.Start()}, \name{lw}, \name{lw\_Locking},
%  \name{lw\_Washing}, \name{ww}, \name{ww\_Waiting}, \name{ww\_Washing}
% \end{flushleft}
% }
% &  \name{lw\_wash.Start()}, \name{ww\_wash.Start()}
%  \\
% \hline $K_2$ &
% &
% \parbox{3.1cm}{
% \begin{flushleft}
% \name{UnLocking}, \name{Washing}, \name{Drying},
% \name{QuickCool()}, \name{wu}, \name{wu\_Washing},
%  \name{wu\_UnLocking}, \name{du}, \name{du\_Drying}, \name{du\_UnLocking}
% \end{flushleft}
% }
% &
% \name{wu\_QuickCool()}, \name{du\_QuickCool()} 
% \\
% \hline
% \end{tabular}
% \end{center}}
% \vspace{-0.2in}
% \end{table}
% Two matching sites for the rule $R_{F}$ in the washing machine
% controller in Fig.~\ref{fig:wash} are shown in Table~\ref{fig:msites} 
% (two more matches, isomorphic to $K_1$ and $K_2$, are not shown for brevity).
% In this table,
% \name{lw} and \name{ww} are the names of the transitions between states
% \name{Locking}/\name{Waiting} and \name{Washing}; while \name{wu} and \name{du}
% are the names of the transitions between states \name{Washing}/ \name{Drying} and
% \name{UnLocking}.  The table says, for example, that in part \mD~of matching
% site $K_1$, \name{t1\_a}=\name{lw\_wash.Start()} and \name{t2\_a}=
% \name{ww\_wash.Start()}.



In the above definition, \mN~denotes the set of all matches within model $M$ of the
\rp{NAC}s of $R$ given the match of \rC~and \rD. If the same \rp{NAC} can match multiple
ways, then all of them are included in \mN~as separate matches.  
\mf{TODO: update:}
For example, if state \name{Washing} had another input transition, that
transition would also appear in \mN~for $K_1$ since it would match $t3$.

The set of matching sites define those places in the model where the rule can
potentially be applied:
\BD[Applicability condition]\label{def:rulecond}
Given a transformation rule $R$, a model $M$, and a matching site
$K = \tuple{$\mN, \mC, \mD$}$,  $R$ is \emph{applicable at $K$}
iff \mN~is empty\footnote{The theory of graph
transformation requires some additional formal preconditions, most notably, the
{\em gluing condition}~\cite{ehrig06}. We so not discuss them here
for brevity.}.
\ED
The above definition ensures that the rule can only be applied at a given site
if \mC~and \mD~are matched and no \rp{NAC} is matched.
\mf{Update:}	
For $R_{F}$, the matching
site $K_1$ given in Table~\ref{fig:msites} does not satisfy the
applicability condition since \mN$_1 \not = \emptyset$.  On the other hand,
no \rp{NAC}s hold in the second matching site, $K_2$.

\begin{figure}[t]
\begin{minipage}[t]{3in}
\begin{tabbing}
b \= bll \= bl \= bl \= bl \= bl \= bl \= bl \= bl \= (Distinctttt) \= \kill
\\
\textbf{Algorithm: Apply Rule} \\
\textbf{Input}: Rule $R$, model $M$, matching site $K= \tuple{$\mN, \mC, \mD$}$\\
\textbf{Output}: Transformed model $M'$\\
\> 1: \> $M' = M$ \\
\> 2: \> {\bf if} \mN~$=\emptyset$ {\bf then} \\
\> 3: \> \> {\bf let} \mA~ be a set of fresh elements corresponding\\
\> \> \> \>  to the part \rA~of $R$ \\
\> 4: \> \> add \mA~to $M'$, \\
\> 5: \> \> remove \mD~from $M'$ \\
\> 6: \> {\bf return} $M'$
\end{tabbing}
\vspace{-0.15in}
\end{minipage}
\caption{Algorithm for applying a graph transformation rule.}
\label{alg:classical}
\vspace{-0.1in}
\end{figure}

\mf{Added term:}
We call rule appliation at a specific matching site that satisfies the
applicability condition, a {\em production}. 

The rule application algorithm is given in Fig.~\ref{alg:classical}.
The applicability condition is checked in Step 2 and if it satisfied, the rule
is applied by adding the elements in \mA~(Step 4) and deleting the elements in
\mD~(Step 5). 
\mf{TODO: update with example}
For example, applying $R_{F}$ to $K_2$ requires the deletion of the action
\name{QuickCool()} from the two transitions because it is contained in \mD, and
the addition of \name{QuickCool()} as an entry action for state
\name{UnLocking} according to \rA.

We refer to rules such as the ones described above as \emph{classical}, to
differentiate them from their \emph{lifted} counterparts which can be applied to
product lines.


\subsection{Software Product Lines}
\label{sec:prodline}
{\bf Michalis and Rick do}


Basic ideas about SPLs: an SPL is a triple: (Feature Model, Domain Model,
Feature Mapping), where the Feature Model describes features and their
relationships, the Domain Model contains the union of all possible model
elemnets adn the Feature Mapping annotates the elements of the Domain Model with
presence conditions such as the features of the feature model are properly
expressed.

We follow the \emph{annotative} product line
approach~\cite{Czarnecki:Antkiewicz:2005,Kastner:Apel:2008,rubin12}, formally
defined below.

%\BD[Product Line]
%A product line $P = \langle \mathsf{FM}, \mathsf{DM}, \mathsf{PC} \rangle$ is a triple, where
%\begin{enumerate}
%\item $\mathsf{FM} = \langle \mathsf{F}, \Phi \rangle$ is a \emph{feature model} consisting of
%a set of features $\mathsf{F}$ and a propositional formula $\Phi$ defined over these features to specify the relationships between them. %$\Phi$ evaluates to true iff a given feature combinations is valid.
%\item $\mathsf{DM}$ is a \emph{domain model} consisting of a set of model elements.
%% \julia{Do we assume anything else on the domain model for the transformations?}
%\item $\mathsf{PC}$ is a \emph{mapping} from $\mathsf{FM}$ to $\mathsf{DM}$ consisting of pairs $\langle \mathtt{E}, \phi_{\mathtt{E}} \rangle$ mapping a domain model element $\mathtt{E} \in \mathsf{DM}$ to a propositional formula $\phi_{\mathtt{E}}$ over the features in $\mathsf{F}$. The formula $\phi_{\mathtt{E}}$ is referred to as the \emph{presence condition} of the element $\mathtt{E}$.
%\end{enumerate}
%\ED

\BD[Product Line]
A product line $P$ consists of the following parts:\\
(1)   A \emph{feature model} that consists of a set of features and a
propositional formula $\Phi_P$ defined over these features to specify the
relationships between them.\\ %$\Phi$ evaluates to true iff a given feature
combinations is valid.
(2) A \emph{domain model} consisting of a set of model elements.\\
% \julia{Do we assume anything else on the domain model for the
% transformations?}
(3) A \emph{mapping} from the feature model to the domain model consisting of
pairs $\langle \mathtt{E}, \phi_{\mathtt{E}} \rangle$ mapping a domain model
element $\mathtt{E}$ to a propositional formula $\phi_{\mathtt{E}}$ over
features. The formula $\phi_{\mathtt{E}}$ is referred to as the \emph{presence
condition} of the element $\mathtt{E}$.  
\ED
For the example, \rs{refer to fig and illustrate}
Relationships between these features are defined by the propositional formula
$\Phi = $  \rs{refer to fig and illustrate}


\rs{Adapt next paragraph:}
In this example, domain model elements are state machine constructs such as
states, transitions, state entry and exit activities, and transition actions.
The presence conditions are given in boxes next to the corresponding domain
model elements, e.g., the state \name{{Waiting}} in Fig.~\ref{fig:wash} is
annotated by the presence condition \feat{Heat}$\vee$\feat{Delay}.
Feature \feat{Wash} is mandatory and thus always occurs.  For simplicity
of presentation, we omit \feat{Wash} from the presence conditions.  We
also do not annotate elements whose
 presence conditions are \emph{true}, e.g., the state \name{{Locking}}.

\BD[Feature Configuration] \label{def:featconfig}
A \emph{valid feature configuration} $\rho$ of a product line $P$ is a subset of
its features that satisfies $\Phi_P$, i.e., $\Phi_P$ evaluates to \emph{true}
when each variable $f$ of $\Phi_P$ is substituted by \emph{true} when $f \in
\rho$ and by \emph{false} otherwise. The set of all valid configurations in $P$
is denoted by $\mathsf{Conf}(P)$.
\ED
\BD[Product Derivation]
A product $M$ is \emph{derived from} the product line $P$ under the feature
configuration $\rho$ if $M$ contains those and only those elements from the
domain model whose presence conditions are satisfied for the features in $\rho$.
\ED

\rs{The next paragraph is a stand-in using a different example. It will be
changed to describe the actual example (see attached document):}
For the example in Fig.~\ref{fig:wash},  sets \{\feat{Wash}, \feat{Heat},
\feat{Dry}\}, \{\feat{Wash}, \feat{Dry}\} and \{\feat{Wash}\} are some of the
valid configurations of the product line $W$.  Any set not containing the
feature \feat{Wash} or containing both \feat{Heat} and \feat{Delay} does not
correspond to a valid configuration as it violates the formula $\Phi_W$ given
above.  The product derived using only the feature \feat{Wash}  will go through
the states \name{{Locking}}, \name{{Washing}} and  \name{{Unlocking}}, while the
product derived using the features \feat{Wash} and \feat{Dry} will go through
the states \name{{Locking}}, \name{{Washing}}, \name{{Drying}} and
\name{{Unlocking}}.


Note that while our work is based on the above definition of annotative product
lines it can readily be adapted to other annotative approaches, e.g.,
CVL~\cite{haugen12}.

\subsection{Lifting of Production Rules}
% \subsection{Transformation Lifting}

% Description (very high level) of what it means to lift a transformation

% This should include an explanation that we are aiming to transform the domain
% model, not the feature model.
\mf{The following is verbatim dump from the product line lifting paper.}
In this section, we describe the process of lifting a transformation rule to
apply to product lines, as defined in~\cite{salay14}. When a classical rule $R$
is adapted for product lines, we say that it is {\em lifted} and denote it by
$\lifted{R}$.

\begin{figure}[t]
\centering
\scalebox{0.25}{\includegraphics[width=0.75\textwidth]{./imgs/commute_cropped.pdf}}
\caption{The preservation of configurations to be satisfied by lifting -- solid
lines denote rule application and dashed lines denote product derivation.}
\label{fig:commute}
\end{figure}

We begin by attempting to define the requirements for $\lifted{R}$, i.e., how it
should act on a product line so that it preserves the effect intended by $R$.  A
natural answer is that after applying $\lifted{R}$, the target product line
should have the same set of products as it would if $R$ were applied separately
to each product  in the source product line. Furthermore, we would expect that
this would also preserve feature configurations. This is illustrated in
Fig.~\ref{fig:commute} -- for each configuration $\rho$, the result should be
the same target product $M'$, regardless of whether $\lifted{R}$ is first
applied followed by the derivation from $P'$, or if $\rho$ is first used to
derive $M$ and then $R$ is applied.  We capture these criteria formally:

\BD [Correctness of lifting] 
\label{def:correctness}
Let a rule $R$ and a product line $P$ be given.  $\lifted{R}$ is a \emph{correct
lifting} of $R$
iff 
(1) for all \emph{rule applications} $P \apply{\lifted{R}} P'$,
$\mathsf{Conf}(P') = \mathsf{Conf}(P)$, and 
(2) for all configurations $\rho$ in $\mathsf{Conf}(P)$,  $M \apply{R} M'$,
where $M$ is derived from $P$, and $M'$ is derived from $P'$ under $\rho$.
\ED

\mf{Unsure whether we need the next paragraph, or whether the citation to
\cite{salay14} is enough.}
This definition is silent on two points. First, it does not  require that the
target feature model be identical to the source feature model; they just need to
be \emph{equivalent}, i.e., have the same set of valid configurations.
However, since $R$ is only defined for the domain model, i.e., it does not
manipulate features, a reasonable expectation is that it should leave the
feature model unchanged. Second, the above definition does not specify exactly
how the domain model should change, as long as the set of products is as
required. The same set of products can be represented by different domain
models and presence conditions~\cite{Rubin:Chechik_Quality:2013}. A reasonable
expectation here is that the domain model should change as little as possible.
These ``expectations'' are not part of the correctness condition since they are
not required to preserve the semantics of $R$; yet, they are ``nice to have''
properties for an implementation of lifting.

\subsection{DSLTrans}
As mentioned in \ref{subsec:model_transformations}, the majority of the
languages in which model transformations are written have the same
expressiveness as any general purpose language. This fact implies the advantage
that, in theory, any computation that can be described in any programming
language can also be described using a model transformation.
DSLTrans~\cite{BarrocaLAFS10} is a model transformation language that
specializes on a particular kind of computations -- for the purpose of this
discussion we will broadly call this class of computations \emph{translations}.
\emph{Translations} include all computations that have as goal the generation of
new model from an input model. Because model transformations are heavily used in
the context of Model-Driven Development (MDD)~\cite{Sendall2003}, these
computations are in general related to software development. Concrete examples
are \emph{code generation}, \emph{refinement}, \emph{reverse engineering},
\emph{migration}, among several others that have been described
in~\cite{LAD+2014}. Such computations have the interesting properties that they
always \emph{terminate} (otherwise they are not meaningful) and are nearly
always required to be \emph{deterministic} (or can be reduced to the
deterministic computation of a set of results). DSLTrans specializes on
\emph{translations} by enforcing these two properties by construction. In other
words, any model transformation described in DSLTrans is guaranteed to terminate
and to be deterministic~\cite{BarrocaLAFS10} because of the way in which
DSLTrans is defined. In order to guarantee these two properties, the
expressiveness of DSLTrans is lower than that of a general-purpose programming
language. Two restrictions are mention worthy: 1) no loops with arbitrary stop
conditions are allowed; and 2) we enforce that transformation rules in a
DSLTrans transformation are divided in layers that execute sequentially. The
rules that compose each of those layers are guaranteed to execute independently
and in parallel from each other.

The expressiveness restrictions present in DSLTans also impose some limitations
on its usage. The most important one is that, because looping is essencially not
allowed, computations modeling reactive systems cannot be expressed in DSLTrans.
The behavior of such systems can be described by using model transformation
rules as the means to update the system's state, thus effectively modeling its
operational semantics. Model transformations of this kind have been named
\emph{simulations} in~\cite{LAD+2014}. 

Despite, there are multiple advantages to a restricted model transformation
language such as DSLTrans. On the one hand, it is often the case for more
expressive transformation languages that properties such as \emph{termination}
and \emph{determinism}  need to be stactically checked on transformations
written in those
languages~\cite{EhrigEhrigTaentzerdeLaraVarroVarro2005,J:Lambers-etAl-2006}. On
the other hand, and more importantly in the context of this paper, such
restrictions have allowed for the development of a verification technique for
DSLTrans model transformations~\cite{Lucio:10}. This verification technique
allows guaranteeing pre- post-condition properties for all executions of a
DSLTrans model transformation by using a static symbolic execution-like
technique~\cite{LOH+14}. More precisely we are able to guarantee that, for all
potential (infinite) executions of a given DSLTrans model transformation, if a
certain pattern of appears in the transformation's input model, then another
pattern will appear in the transformation's output model. We have been able to
demonstrate the applicability and efficiency of our verification technique when
analysing a case study transformation extracted from General
Motors~\cite{selimICGT2014}. 

\subsection{GM-to-AUTOSAR Model Transformation}
%%{\bf Gehan does}
\input{background_GM2AUTOSAR}
